(PushArgs 
\\[0ex][`f`,term\_to\_arg $f$ 
\\[0ex];`T`,term\_to\_arg $T$ 
\\[0ex];`n`,var\_to\_arg `n' 
\\[0ex]
\\[0ex];`nn`,var\_to\_arg `nn' 
\\[0ex];`S`,term\_to\_arg $S$ 
\\[0ex];`i`,int\_to\_arg 8 
\\[0ex]
\\[0ex];`RangeIndTac`, tactic\_text\_to\_arg (itext\_term "(WFndHypInd 5 ({-}1))") 
\\[0ex]])